(0) Obligation:

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).

Query: goal()

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:


Clauses:


Afs:

(3) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(4) YES